/*@ i>0 */
int f(int i)
{
  int j;
  j = i+1;
  j = 2*j;
  return j;
}
/*@ result > 2*/
